Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		app(app(:,app(app(:,x),y)),z)	→ app(app(:,x),app(app(:,y),z))
2:		app(app(:,app(app(+,x),y)),z)	→ app(app(+,app(app(:,x),z)),app(app(:,y),z))
3:		app(app(:,z),app(app(+,x),app(f,y)))	→ app(app(:,app(app(g,z),y)),app(app(+,x),a))

There are 14 dependency pairs:


4:		APP(app(:,app(app(:,x),y)),z)	→ APP(app(:,x),app(app(:,y),z))
5:		APP(app(:,app(app(:,x),y)),z)	→ APP(app(:,y),z)
6:		APP(app(:,app(app(:,x),y)),z)	→ APP(:,y)
7:		APP(app(:,app(app(+,x),y)),z)	→ APP(app(+,app(app(:,x),z)),app(app(:,y),z))
8:		APP(app(:,app(app(+,x),y)),z)	→ APP(+,app(app(:,x),z))
9:		APP(app(:,app(app(+,x),y)),z)	→ APP(app(:,x),z)
10:		APP(app(:,app(app(+,x),y)),z)	→ APP(:,x)
11:		APP(app(:,app(app(+,x),y)),z)	→ APP(app(:,y),z)
12:		APP(app(:,app(app(+,x),y)),z)	→ APP(:,y)
13:		APP(app(:,z),app(app(+,x),app(f,y)))	→ APP(app(:,app(app(g,z),y)),app(app(+,x),a))
14:		APP(app(:,z),app(app(+,x),app(f,y)))	→ APP(:,app(app(g,z),y))
15:		APP(app(:,z),app(app(+,x),app(f,y)))	→ APP(app(g,z),y)
16:		APP(app(:,z),app(app(+,x),app(f,y)))	→ APP(g,z)
17:		APP(app(:,z),app(app(+,x),app(f,y)))	→ APP(app(+,x),a)

The approximated dependency graph contains one SCC: {4,5,7,9,11,13,15,17}.

Consider the SCC {4,5,7,9,11,13,15,17}. By taking the AF π with π(app) = π(APP) = 1 together with the lexicographic path order with precedence : ≻ + and : ≻ g, the rules in {1,3-5,9,11,13} are weakly decreasing and the rules in {2,7,15,17} are strictly decreasing. There is one new SCC.
- Consider the SCC {4,5,9,11,13}. The constraints could not be solved.

Tyrolean Termination Tool (0.21 seconds) --- May 4, 2006